Ja, gut. Also weiter im Text. Nur noch mal zur Erinnerung. Wir hatten angeschnitten letztes Mal

das Kapitel Kodaten oder Kodatentypen. Ja, wir hatten uns angesehen ein Beispiel, eine

korekursive Definition einer Map-Funktion über Streams und wir hatten uns klar gemacht,

dass diese korekursive Definition im Wesentlichen auf einem Morphismusbegriff zu beruhen scheint,

der dual ist zu dem, den wir schon gesehen haben für Sigma-Algebrien. So, wir erinnern uns an die

Geschichte mit den Mengenkonstruktionen, das mit kathesischem Produkt und des Jungter Vereinigungen

und solchen Dingen. Wir machen das jetzt so ein bisschen formaler, wir führen also für diese

Dinger mal so eine Art Syntax ein. Das heißt, wir geben uns mal einen Metabuchstaben G und vielleicht

noch F oder sowas und wir definieren die Dinger jetzt also über eine Grammatik. Also, wir fangen

an mit der ersten Alternative. Also eine Mengenkonstruktion kann etwas sein, was seine

Argumente ganz ignoriert und einfach eine fest gewählte Menge A zurückgibt.

Dann kann eine Mengenkonstruktion Identität sein, wobei eben die identische Mengenkonstruktion ist,

diejenige ist, die eine Menge nimmt und genau diese Menge wieder zurückgibt.

So, dann kann eine Mengenkonstruktion eine Summe von zwei Mengenkonstruktionen sein oder ein Produkt.

So, das ist jetzt also unsere Syntax, in Anführungsstrichen, für Mengenkonstruktionen.

vice versa

Die Sementik, die setze ich auch wieder in Anführungsstriche, deswegen weil ich zwischen Syntax und Sementik bei diesen Dingern gar nicht so genau unterscheide.

Ja, die Sementik von diesen Ausdrücken ist eben als tatsächliche Mengenkonstruktion.

Das heißt, ich muss sagen, was macht so ein Ausdruck mit einer Menge?

Also zum Beispiel, wenn ich A auf eine Menge x anwende, wie ich angedeutet hatte, ignoriert sie dieses Argument einfach und gibt eben A zurück.

Auch Identität hatten wir schon angedeutet.

Das bedeutet dann Summe zweier Mengenkonstruktionen g und f angewendet auf eine Menge x ist einfach gx plus fx.

Und genauso für Produkt g Kreuz f angewendet auf x ist per Definition gleich gx Kreuz fx.

So, und das Entscheidende ist eben, dass wir genauso die Anwendung von g auf eine Abbildung definieren.

G auf eine Abbildung f und wenn f, sagen wir mal, eine Abbildung von x nach y ist, dann ist mit eben wörtlich derselben Definition, wie hier,

nur eben überall mit x durch f ersetzt, dann ist gf eine Abbildung von gx nach gy.

Für die, die es interessiert, g ist also ein Funktur, fehlt noch eine Eigenschaft, aber egal.

Gut, so jetzt haben wir uns also ein bisschen Ausdrucksmittel verschafft, um jetzt über diese Mengenkonstruktionen zu reden.

So, wir erinnern uns nochmal ans vorige Kapitel zurück.

Da hatten wir uns Gedanken gemacht eben über Sigma-Algebrin und ihre Homomorphismen.

So, und das Entscheidende dabei war, wir hatten so ein Funktur, jetzt habe ich es doch gesagt, also jetzt haben wir eine Mengenkonstruktion definiert,

f Sigma, die auf einer Menge x agiert, indem sie die Summe bildet über alle Operationen f in Sigma.

Das hier ist Summe, das ist Sigma, hatten wir uns damals klar gemacht, über x hoch n, wobei n die Arität der Operation ist.

Und dann haben wir gesagt, eine Sigma-Algebra mit Trägermenge m ist einfach eine Abbildung alpha von diesem f Sigma m nach m.

Und wenn ich noch eine Sigma-Algebra beta mit Trägermenge n habe, sprich eine Abbildung von f Sigma n nach n,

dann ist eine Abbildung h von m nach n genau dann ein Sigma-Homomorphismus, in dem Sinne, den wir vorher definiert hatten,

sprich h verträgt sich mit allen Operationen der Signatur Sigma, wenn das Diagramm, was ich bekomme,

wenn ich f Sigma jetzt als Kombination von Plus- und Mal-Operationen, ja und vielleicht einer konstanten Menge und so weiter,

wenn ich das jetzt anwende auf h, das haben wir jetzt formal definiert, was das heißt, ja das war letztes Mal so ein bisschen informell,

das haben wir jetzt formal definiert, wenn also f Sigma von h dieses Diagramm hier zum Kommutieren bringt.

So, nicht an dieses f Sigma, das ist genauso eine Mengenkonstruktion wie das, was wir gerade definiert haben, das passt in unsere Grammatik,

wir haben hier das x, das kommt hier vom Identitätsfunktor, wir bilden hier Kreuzprodukte von dem Ding mit sich selbst n mal, wenn n die Arität ist,

wir bilden hier bisjunkte Vereinigungen, also Plus hier geschrieben als Summe, das ist also ein Beispiel praktisch unseres gerade eingeführten Begriffs von Mengenkonstruktion,

also von syntaktischer Mengenkonstruktion. So und jetzt eben dualisieren wir das alles, wir hatten letztes Mal gesehen,

dass also die Menge der Streams über a, die hatten wir geschrieben a hoch Omega, das ist also die Menge der Streams,

wo die also nacheinander immer wieder Elemente aus a ausspucken, dass die diese Struktur hier hat, wo wir also das kompliziert zusammengesetzte Ding

nicht mehr auf der linken Seite des Pfeils, sondern auf der rechten Seite des Pfeils sehen, jetzt mal ganz blöd und rein auf die Typografie guckend gesprochen.

So und dieses Prinzip, das verallgemeinern wir jetzt.

So wir haben bisher gesprochen über Algebrin, jetzt sprechen wir also, Co dreht alle Pfeile um, über Co-Algebrin und zwar für so eine Mengenkonstruktion G.

So das definiere ich jetzt wie gesagt also einfach umgekehrt, ich wende also jetzt die Mengenkonstruktion nicht mehr auf der linken Seite an,